@InProceedings{CousotCousot77,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Abstract interpretation: a unified lattice model for static
                analysis of programs by construction or approximation of
              fixpoints},
   booktitle = {{ACM POPL'77}},
   publisher = {ACM Press}
}
%   address =   {Los Angeles},
%   booktitle = {Conference Record of the Fourth  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
@inCollection{CousotCousot04-WCC,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Basic Concepts of Abstract Interpretation},
   booktitle = {Building the Information Society},
   chapter =   4,
   publisher = {Kluwer},
   pages =     {359--366},
   year =      2004,
   baseurl =   {http://www.di.ens.fr/~cousot/COUSOTpapers/WCC04.shtml},
}
%   editor =    {P{.}~Jacquart},
%   publisher = {Kluwer},
@incollection{LeinoBoogie,
   author =    {M{.} Barnett and B{.}-Y{.}E{.} Chang and R{.} DeLine and
                B{.} Jacobs and K{.}R{.}M{.} Leino},
   title =     {Boogie: A Modular Reusable Verifier for Object-Oriented Programs},
   booktitle = {FMCO'05}
}
%   isbn =      {3-540-36749-7}
%   editor =    {F{.}S{.} de Boer and M{.}M{.} Bonsangue and S{.} Graf and W{.}P{.} de Roever},
%   booktitle = {Proceedings of the Fourth International Conference  on Formal Methods for Components and Objects, FMCO$\,$'{2005}},
%   series =    {Amsterdam, 1--4 November  2005, Lecture Notes in Computer Science  4111},
@inproceedings{z3BjornerDeMoura,
   author =    {L{.}M{.}~de Moura and N{.}~Bj{\o}rner},
   title =     {{Z3}: An Efficient {SMT} Solver.},
   series =    {LNCS 4963},
   booktitle = {TACAS'08},
   year =      2008,
   pages =     {337--340},
   publisher = {Springer},
}
%   isbn =      {978-3-540-78799-0},
%   month =     {29 March ---6 April },
%   editor =    {C{.}R{.}~Ramakrishnan and J{.}~Rehof},
%   booktitle = {Proceedings of the Fourteenth International Conference  on Tools and Algorithms for the Construction and Analysis of Systems, TACAS$\,$'{08}},
@inproceedings{FlanaganQadeer02-POPL,
   author =    {C{.} Flanagan and S{.} Qadeer},
   title =     {Predicate abstraction for software verification},
   pages =     {191--202},
   booktitle = {29th POPL},
   publisher = {ACM Press},
   year =      2002,
}
%   address =   {Portland},
%   booktitle = {Conference Record of the Twentyninth  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
%   month =     {January },
@InProceedings{CousotCousot79-1-POPL,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Systematic design of program analysis frameworks},
   booktitle = {ACM POPL'79},
}
%   address =   {San Antonio},
%   booktitle = {Conference Record of the Sixth  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
@inproceedings{GopanRepsSagivPOPL05,
   author =    {D{.} Gopan and T{.}W{.}. Reps and S{.} Sagiv},
   title =     {A framework for numeric analysis of array operations},
   pages =     {338--350},
   booktitle = {32nd POPL},
   publisher = {ACM Press},
   year =      2005,
}
%   address =   {San Diego},
%   booktitle = {Conference Record of the Twentyfifth  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
%   month =     {19--21 January },
@inProceedings{Halbwachsperon-PLDI08,
   author =    {N{.} Halbwachs and M{.} P{\'e}ron},
   title =     {Discovering properties about arrays in simple programs},
   pages =     {339--348},
   booktitle = {PLDI'2008},
   publisher = {ACM Press},
   year =      2008,
}
%   address =   {San Diego},
%   booktitle = {Proceedings of the  ACM SIGPLAN$\,$'2008 Conference  on Programming Language Design and Implementation (PLDI)},
%   month =     {7--13 June },
%   editor = {R{.} Gupta and S{.}P{.} Amarasinghe},
@InProceedings{GulwaniEtAL-POPL08,
   author =    {S{.} Gulwani and B{.} McCloskey and A{.} Tiwari},
   title =     {Lifting abstract interpreters to quantified logical domains},
   booktitle = {35th POPL},
   pages =     {235--246},
   publisher = {ACM Press},
   year =      2008,
}
%   address =   {San Francisco},
%   booktitle = {Conference Record of the Fourth  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
%   month = {7-12 January },
%   editor = {G{.}C{.} Necula and Ph{.} Wadler},
@inproceedings{Dill89-1,
   author =    {Dill, D.L{.}},
   title =     {Timing assumptions and verification of finite-state concurrent
                systems},
   booktitle = {Automatic Verification Methods for Finite State Systems},
   series =    {LNCS  407},
   publisher = {Springer},
   pages =     {197--212},
   year =      1989,
}
%   editor =    {Sifakis, J{.}},
@techReport{Pratt77-1,
   author =      {V.R{.} Pratt},
   title =       {Two Easy Theories Whose Combination is Hard},
   institution = {MIT},
   year =        1977,
   note = {\url{boole.stanford.edu/pub/sefnp.pdf}},
}
%   month = {september  1,},
@article{Roy59-CRAS,
   author =  {B{.} Roy},
   title =   {Transitivit{\'e} et connexit{\'e}},
   journal = {Comptes\discretionary{-}{}{-}Rendus de l'Acad{\'e}mie des Sciences de Paris, S{\'e}r{.} A-B},
   volume =  249,
   pages =   {216--218},
   year =    1959,
}
%   month =       {19 May },
@article{LeeCho03-EL,
   author =  {S{.}-H{.} Lee and  D{.}-H{.} Cho},
   title =   {Packet-scheduling algorithm based on priority of separate buffers for unicast and multicast services},
   journal = {Electronics Letters},
   volume =  39,
   number =  2,
   pages =   {259--260},
   year =    2003,
}
%   month =   {23 January },
@article{SongEtAl07-routing,
   author =  {W.-Z{.} Song and F{.} Yuan and R{.} LaHusen and B{.} Shirazi},
   title =   {Time-optimum packet scheduling for many-to-one routing in wireless sensor networks},
   journal = {Int.\ J.\ of Parallel, Emergent and Distributed Systems},
   volume =  22,
   number =  5,
   pages =   {355--370},
   year =    2007,
}
@inproceedings{Kildall73-1,
   author =    {Kildall, G{.}},
   title =     {A Unified Approach to Global Program Optimization},
   booktitle = {1st POPL},
   publisher = {ACM Press},
   year =      1973,
   pages =     {194--206},
}
%   address =   {Boston},
%   booktitle = {Conference Record of the First  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
%   month =     {October },
@inProceedings{KovacsVoronkov09-FASE,
   author =    {L{.} Kov{\'a}cs and A{.} Voronkov},
   title =     {Finding Loop Invariants for Programs over Arrays Using a Theorem Prover},
   booktitle = {FASE'2009},
   series =    {LNCS 5503},
   publisher = {Springer},
   pages =     {470--485},
   year =      2009,
}
%   booktitle = {Proceedings of the  Fundamental Approaches to Software Engineering, Twelfth International Conference , FASE 2009},
%   month =     {March  22--29},
%   editor =    {M{.} Chechik and M{.} Wirsing},
@inproceedings{GopanReps-CAV06,
   author =    {D{.} Gopan and T{.}W{.}. Reps},
   title =     {Lookahead Widening},
   booktitle = {CAV'06},
   pages =     {452--466},
   series =    {LNCS 4144},
   publisher = {Springer},
   year =      2006,
}
%   booktitle = {Proceedings of the Eightteenth International Conference  on Computer Aided Verification, CAV$\,$'{2006}},
%   month =     {17--20 August },
%   editor =    {T{.} Ball and R{.}B{.} Jones},
@incollection{ChalinEtAl-FMCO05,
   author =    {P{.} Chalin and J{.}R{.} Kiniry and G{.}T{.} Leavens and E{.} Poll},
   title =     {Beyond Assertions: Advanced Specification and Verification with {JML} and {ESC/Java2}},
   pages =     {77--101},
   booktitle = {FMCO'05},
   series =    {LNCS 4111},
   year =      2006,
   publisher = {Springer},
}
%   isbn =      {3-540-36749-7}
%   booktitle = {Proceedings of the Fourth International Conference  on Formal Methods for Components and Objects, FMCO$\,$'{2005}},
%   editor =    {F{.}S{.} de Boer and M{.}M{.} Bonsangue and S{.} Graf and W{.}P{.} de Roever},
@article{BernardeschiEtAl-JSS97,
   author =  {C{.} Bernardeschi and A{.} Fantechi and S{.} Gnesi},
   title =   {An industrial application for the {JACK} environment},
   journal = {J.\ of Systems and Software},
   volume =  39,
   number =  3,
   pages =   {249--264},
   year =    1997,
}
@inproceedings{FilliatreMarche:CAV07,
   author =    {J{.}-C{.} Filli{\^a}tre and C{.} March{\'e}},
   title =     {The {Why/Krakatoa/Caduceus} Platform for Deductive Program Verification},
   series =    {LNCS 4590},
   booktitle = { CAV'07},
   publisher = {Springer},
   year =      2007,
   pages =     {173--177},
}
%   isbn =      {978-3-540-73367-6},
%   booktitle = {Proceedings of the Ninthteenth International Conference  on Computer Aided Verification, CAV$\,$'{07}},
%   month =     {3--7 July },
%   editor =    {W{.} Damm and H{.} Hermanns},
@inproceedings{BarnettLeinoSchulte:CASSIS04,
   author =    {M{.} Barnett and K{.}R{.}M{.} Leino and W{.} Schulte},
   title =     {The {S}pec\# programming system: An overview},
   booktitle = {CASSIS'04},
   series =    {LNCS 3362},
   publisher = {Springer},
   year =      2005,
   pages =     {49--69},
}
%   booktitle = {Proceedings of the International Workshop  on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS'{2004}},
%   month =     {10-14 March  2004},
%   editor =    {Barthe, G. and Burdy, L. and Huisman, M. and Lanet, J.-L. and Muntean, T.},

@ inproceedings{Cousot03-ZM,
   author =    {P{.} Cousot},
   title =     {Verification by Abstract Interpretation},
   booktitle = {Verification -- Theory \& Practice},
   series =    {LNCS 2772},
   publisher = {Springer},
   pages =     {243--268},
   year =      2003,
}
%   baseurl =   {http://www.di.ens.fr/~cousot/COUSOTpapers/Zohar03.shtml},
%   isbn =      {3-540-21002-4},
%   booktitle = {Proceedings of the International Symposium  on Verification -- Theory \& Practice  -- Honoring Zohar Manna's 64th Birthday},
%   address =   {Taormina},
%   month =     {29 June -- 4 July },
%   editor =    {N{.} Dershowitz},

@inCollection{Allamigeon-ESOP08,
   author =    {X{.} Allamigeon},
   title =     {Non-disjunctive Numerical Domain for Array Predicate Abstraction},
   booktitle = {ESOP'08},
   series =    {LNCS 4960},
   pages =     {163--177},
   publisher = {Springer},
   year =      2008,
}
%   booktitle = {Proceedings of the Seventeenth  European Symposium on Programming Languages and Systems, ESOP$\,$'{2008}, Budapest},
%   month =     {March  29--April  6},
%   editor =    {S{.} Drossopoulou},

@inproceedings{ArmandoBenerecettiMantovani-TACAS07,
   author =    {A{.} Armando and M{.} Benerecetti and J{.} Mantovani},
   title =     {Abstraction Refinement of Linear Programs with Arrays},
   booktitle = {TACAS'07},
   series =    {LNCS  4424},
   year =      2007,
   pages =     {373--388},
   publisher = {Springer},
}
%   booktitle = {Proceedings of the Thirteenth International Conference  on Tools and Algorithms for the Construction and Analysis of Systems, TACAS$\,$'{2007}},
%   month =     {24 March ---1 April },
%   editor =    {O{.} Grumberg and M{.} Huth},

@inProceedings{BradleyMannaSipma06-array,
   author =    {A.R{.} Bradley and Z{.} Manna and H.B{.} Sipma},
   title =     {What's Decidable About Arrays?},
   booktitle = {VMCAI'06},
   series =    {LNCS  3855},
   publisher = {Springer},
   pages =     {427--442},
   year =      2006,
}
%   address =   {Charleston},
%   booktitle = {Proceedings of the Seventh International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI {2006})},
%   month =     {8--10, January },

@article{LahiriBryant-TCL07,
   author =  {S{.}K{.} Lahiri and R{.}E{.} Bryant},
   title =   {Predicate abstraction with indexed predicates},
   journal = {ACM Trans{.} Comput{.} Log{.}},
   volume =  9,
   number =  1,
   pages =   {Art.~4},
   year =    2007,
}
%   month =   {December },

@inCollection{SeghirPodelskiWies-SAS09,
   author =    {M{.}N{.} Seghir and A{.} Podelski and T{.} Wies},
   title =     {Abstraction Refinement for Quantified Array Assertions},
   year =      2009,
   booktitle = { SAS'09},
   series =    {LNCS  5673},
   publisher = {Springer},
   pages =     {3--18},
}
%   booktitle = {Proceedings of the Sixteenth International Symposium  on Static Analysis, SAS$\,$'{2009}},
%   editor =    {J{.} Palsberg and Z{.} Su},
%   month =     {8--10 september },

@InProceedings{JhalaMcMillan-CAV-07,
   author =    {R{.} Jhala and K{.}L{.} McMillan},
   title =     {Array Abstractions from Proofs},
   series =    {LNCS  4590},
   booktitle = {CAV'07},
   publisher = {Springer},
   year =      2007,
   pages =     {193--206},
}
%   booktitle = {Proceedings of the Thirteenth International Conference  on Computer Aided Verification, CAV$\,$'{07}},
%   editor =    {W{.} Damm and H{.} Hermanns},
%   month =     {July },

@InProceedings{XuPeytonJonesClaessen09-POPL,
   author =    {D{.}N{.} Xu and S{.}L{.} Peyton Jones and K{.} Claessen},
   title =     {Static contract checking for {H}askell},
   pages =     {41--52},
   booktitle = {36th POPL},
   publisher = {ACM Press},
   year =      2009,
}
%   address =   {Savannah},
%   booktitle = {Conference Record of the Thirtysixth  Annual ACM SIGPLAN\discretionary{-}{}{-}SIGACT Symposium on Principles of Programming Languages},
%   editor = {Z{.} Shao and B{.}C{.} Pierce},

@inProceedings{MarronEtAL07-PASTE,
   author =    {M{.} Marron and D{.} Stefanovic and M{.}V{.} Hermenegildo and D{.} Kapur},
   title =     {Heap analysis in the presence of collection libraries},
   pages =     {31--36},
   booktitle = {PASTE'07},
   publisher = {ACM Press},
   year =      2007,
}
%   address =   {San Diego},
%   booktitle = {Proceedings of the Seventh  ACM SIGPLAN-SIGSOFT Workshop  on Program Analysis for Software Tools and Engineering, PASTE$\,$'{07}},
%   editor =    {M{.} Das and D{.} Grossma},
%   month =     {7--14 June },

@inProceedings{MarronEtAL08-PASTE,
   author =    {M{.} Marron and M{.} M{\'e}ndez-Lojo and M{.}V{.} Hermenegildo and D{.} Stefanovic and D{.} Kapur},
   title =     {Sharing analysis of arrays, collections, and recursive structures},
   pages =     {43--49},
   booktitle = {PASTE'08},
   publisher = {ACM Press},
   year =      2008,
}
%   address =   {Atlanta},
%   booktitle = {Proceedings of the Eight  ACM SIGPLAN-SIGSOFT Workshop  on Program Analysis for Software Tools and Engineering, PASTE$\,$'{08}},
%   editor =    {S{.} Krishnamurthi and M{.} Young},
%   month =     {9--10 November },

@inProceedings{MarronEtAL09-ISMM,
   author =    {M{.} Marron and D{.} Kapur and M{.}V{.} Hermenegildo},
   title =     {Identification of logically related heap regions},
   pages =     {89--98},
   booktitle = {ISMM'09},
   publisher = {ACM Press},
   year =      2009,
}
%   address =   {Dublin},
%   booktitle = {Proceedings of the Eight  International Symposium on Memory Management, ISMM$\,$'{2009}},
%   editor =    {H{.} Kolodner, G{.}L{.} Steele Jr{.}},
%   month =     {19--20 June },

@phdThesis{DenisGopan-PhD2007,
   author = {D{.} Gopan},
   title =  {Numeric program analysis techniques with applications to array analysis and library summarization},
   school = {University of Wisconsin at Madison,  Madison, WI, USA},
   pages = {231},
   year =   2007,
}
%   isbn = {978-0-549-19582-5},

@inproceedings{McMillan-TACAS08,
  author    = {K{.} L{.} McMillan},
  title     = {Quantified Invariant Generation Using an Interpolating Saturation
               Prover},
  booktitle = {TACAS'08},
  series    = {LNCS  4963},
  publisher = {Springer},
  year      = {2008},
  pages     = {197--212},  
}
%  booktitle = {Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of
               Systems},
%  editor    = {C{.} R{.} Ramakrishnan and J{.} Rehof},
%  month     = {April},

@inproceedings{Logozzo-SAS03,
  author    = {F{.} Logozzo},
  title     = {Class-Level Modular Analysis for Object Oriented Languages},
  series    = {LNCS 2694},
  booktitle = {SAS'03},
  publisher = {Springer},
  year      = {2003},
  pages     = {37--54},
}
%  booktitle = {Proceedings of the 10th Static Analysis Symposium},
%  editor    = {R{.}  Cousot},
%  month     = {June},

@inproceedings{BarnettFahndrichLogozzo-SAC10,
  author    = {M{.} Barnett and M{.} F{\"a}hndrich and F{.} Logozzo},
  title     = {Embedded Contract Languages},
  booktitle = {SAC'10},
  publisher = {ACM Press},
  year =      2010,
}
%  address =   {Lausanne, Switzerland},
%  booktitle = {Proceedings of the {ACM} Symposium on Applied Computing},
%  pages = {???-???},
%  editor    = {???},
% month =     {22--26 March },


@inproceedings{FerraraLogozzoFahndrich-OOPSLA08,
  author = {P{.} Ferrara and F{.} Logozzo and M{.} F{\"a}hndrich},
  title  = {Safer Unsafe Code in .{NET}},
  booktitle = {OOPSLA'08},
  year    = 2008,
  publisher = {ACM Press},
}
%  address =   {Nashville, USA},
%  booktitle = {Proceedings of the {ACM} Conference on Object-Oriented Programming, Systems, Languages and Applications},

@inproceedings{BeyerEtAl-PLDI07,
  author    = {D{.} Beyer and
               T{.} A{.} Henzinger and
               R{.} Majumdar and
               A{.} Rybalchenko},
  title     = {Path invariants},
  booktitle = {PLDI'07},
  publisher = {ACM Press},  
  year      = {2007},
  pages     = {300--309},
}
%  booktitle = {Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation},
%  editor    = {J{.} Ferrante and K{.} S{.} McKinley},
@article{Mine-HOSC06,
   author =    {Min\'e, A{.}},
   title =   {The Octagon Abstract Domain},
   journal = {Higher-Order and Symbolic Computation},
   volume = 19,
   pages = {31--100},
   year =    2006,
   baseurl = {http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf},
}
@article{Shostak81-JACM,
   author =  {R{.} Shostak},
   title =   {Deciding Linear Inequalities by Computing Loop Residues},
   journal = {JACM},
   volume =  28,
   number =  4,
   pages =   {769--779},
   year =    1981,
}
%   journal = {Journal of the Association for Computing Machinery},
%   month =   {October },
@techReport{GarminDevice06,
   author =      {{Garmin Int.}},
   title =       {Garmin Device Interface Specification},
   institution = {Garmin Int., Inc., Olathe},
   year =        2006,
   note =        {\url{www.garmin.com/support/pdf/iop_spec.pdf}},
}
%   month =       {19 May },
@phdthesis{Logozzo-PhD,
   author =  {Logozzo, F{.}},
   title =   {Modular static analysis of object-oriented languages},
   school =  {{\'E}co\-le po\-ly\-tech\-ni\-que},
   type =    {Th{\`e}\-se de doc\-to\-rat en in\-for\-ma\-ti\-que},
   year =    2004,
   baseurl =   {http://www.imprimerie.polytechnique.fr/Theses/Files/Logozzo.pdf},
}
%address = {Pa\-lai\-seau},
%   month =   {15 June },
@InProceedings{DilligDilligAiken-ESOP10,
  author = 	 {I{.} Dillig and T{.} Dillig and A{.} Aiken},
  title = 	 {Fluid Updates: Beyond Strong vs. Weak Updates},
  booktitle = {ESOP'10},
  pages = 	 {246--266},
  year = 	 {2010},
  series    = {LNCS  6012},
  publisher = {Springer},
}
%  booktitle = {Proceedings of the 19th Symposium on Programming (ESOP'10)},
%  month     = {March}
%  editor = 	 {A{.} Gordon},
@book{eiffel,
   author =    {B.~Meyer},
   title =     {Eiffel: The Language},
   publisher = {Prentice Hall},
   year =      1991,
}

@inproceedings{CousotHalbwachs78,
   author =    {Cousot, P{.} and Halbwachs, N{.}},
   title =     {Automatic discovery of linear restraints among variables of
                a program},   
   booktitle = {ACM POPL '78}
}

@inproceedings{ClarisoCortadella04,
  author    = {R{.} Claris{\'o} and J{.} Cortadella},
  title     = {The Octahedron Abstract Domain},
  booktitle = {SAS'04}
}

@inproceedings{Mine02,
  author    = {Min{\'e}, A{.}},
  title     = {A Few Graph-Based Relational Numerical Abstract Domains},
  booktitle = {SAS'02}
}
@inproceedings{LavironLogozzo9,
  author    = {Laviron, V{.} and
               Logozzo, F{.}},
  title     = {Refining Abstract Interpretation-Based Static Analyses with
               Hints},
  booktitle = {APLAS'09},
}

@article{Karr76,
  author    = {Michael Karr},
  title     = {Affine Relationships Among Variables of a Program},
  journal   = {Acta Inf.},
  volume    = {6},
  year      = {1976}
}

@inproceedings{Sankaranarayanan07,
  author    = { Sankaranarayanan, S{.} and
               Ivancic, F{.} and
               Gupta, A{.}},
  title     = {Program Analysis Using Symbolic Ranges},
  booktitle = {SAS'07},
}

@inproceedings{FeretEtAl06,
  author    = {Cousot, P{.} and
               Cousot, R{.} and
               Feret, J{.} and
               Mauborgne, L{.} and
               Min{\'e}, A{.} and
               Monniaux, D{.} and
               Rival, X{.}},
  title     = {Combination of Abstractions in the ASTR{\'E}E Static
               Analyzer},
  booktitle = {ASIAN'06}
}

@article{KhachiyanBBEG08,
  author    = {Khachiyan, L{.} and
               Boros, E{.} and
               Borys, E{.} and
               Elbassioni, K{.} M{.} and
               Gurvich, V{.}},
  title     = {Generating All Vertices of a Polyhedron Is Hard},
  journal   = {Discrete {\&} Computational Geometry},
  volume    = {39},
  number    = {1-3},
  year      = {2008},
  pages     = {174-190}
}

@inproceedings{LavironLogozzo09-1,
  author    = {Laviron, V{.} and
               Logozzo, F{.}},
  title     = {SubPolyhedra: A (More) Scalable Approach to Infer Linear
               Inequalities},
  booktitle = {VMCAI'09},
}

@inproceedings{Mine04,
  author    = {Min{\'e}, A{.}},
  title     = {Relational Abstract Domains for the Detection of Floating-Point
               Run-Time Errors},
  booktitle = {ESOP'04}
}

@inproceedings{TillmannPeli08,
  author    = {Tillmann, N{.} and
               de Halleux, J{.}},
  title     = {Pex-White Box Test Generation for {.Net}},
  booktitle = {TAP'08}
}

@misc{codecontracts,
  author = 	 {F\"ahndrich, M{.} and  Barnett, M{.} and  Logozzo, F{.}},
  title = 	 {{Code Contracts}},
  url = "http://research.microsoft.com/contracts",
  month = 	 mar,
  year = 	 {2009} 
}

@inproceedings{embedded-cc-sac-oops-2010,
 author = {F\"ahndrich, M{.} and  Barnett, M{.} and  Logozzo, F{.}},
 title = {Embedded contract languages},
 booktitle = {ACM SAC'10},
 year = {2010},
 }

@Misc{ecma,
  author = 	 {{ECMA}},
  title = 	 {Standard {ECMA-355}, {C}ommon {L}anguage {I}nfrastructure },
  month = 	 jun,
  year = 	 {2006} 
}




@inproceedings{LogozzoMaf08,
  author    = {F{.} Logozzo and
               M{.} F{\"a}hndrich},
  title     = {On the Relative Completeness of Bytecode Analysis Versus
               Source Code Analysis},
  booktitle = {CC'08}
}



@InProceedings{MafLogozzo10,
  author = 	 {M{.} F{\"a}hndrich and F{.} Logozzo},
  title = 	 {Static contract checking with Abstract Interpretation},
  booktitle = {FoVeOOS'10},
  year = 	 {2010},
  series = 	 {LNCS},
  publisher = {Springer-Verlag}
}

@inproceedings{SimonKing02,
  author    = {A{.} Simon and
               A{.} King and
               J{.} M{.} Howe},
  title     = {Two Variables per Linear Inequality as an Abstract Domain},
  booktitle = {LOPSTR'02}
}

@inproceedings{LogozzoFahndrich08-2,
  author    = {F{.} Logozzo and
               M{.} F{\"a}hndrich},
  title     = {Pentagons: a weakly relational abstract domain for the efficient
               validation of array accesses},
  booktitle = {ACM SAC'08}
}

@inproceedings{astree,
  author    = {B{.} Blanchet and
               P{.} Cousot and
               R{.} Cousot and
               J{.} Feret and
               L{.} Mauborgne and
               A{.} Min{\'e} and
               D{.} Monniaux and
               X{.} Rival},
  title     = {A static analyzer for large safety-critical software},
  booktitle = {PLDI'03}
}

@inproceedings{Mine06,
  author    = {Min{\'e}, A{.}},
  title     = {Symbolic Methods to Enhance the Precision of Numerical Abstract
               Domains},
  booktitle = {VMCAI'06},
  year      = {2006},
}

@inproceedings{CousotCousot-92,
  author    = {Cousot, P{.} and
               Cousot, R{.}},
  title     = {Comparing the Galois Connection and Widening/Narrowing Approaches
               to Abstract Interpretation},
  booktitle = {PLILP'92}
 }
}

@inproceedings{ESCJava,
  author    = {Flanagan, C{.} and
               Leino, K{.} R{.} M{.} and
               Lillibridge, M{.} and
               Nelson, G{.} and
               Saxe, J{.} B{.} and
                Stata, R{.}},
  title     = {Extended Static Checking for Java},
  booktitle = {ACM PLDI'02},
}


@inproceedings{Jack,
  author    = { Barthe, G{.} and
                Burdy, L{.} and
               Charles, J{.} and
               Gr{\'e}goire, B{.} and
               Huisman, M{.} and
               Lanet, J{.}-L{.} and
                Pavlova, M{.} and
               Requet, A{.}},
  title     = {{JACK} - A Tool for Validation of Security and Behaviour of
               {J}ava Applications},
  booktitle = {FMCO'06}
}

@inproceedings{Why,
  author    = { Filli{\^a}tre, J{.}-C{.} and
               March{\'e}, C{.}},
  title     = {The {W}hy/{K}rakatoa/{C}aduceus Platform for Deductive Program
               Verification},
  booktitle = {CAV'07}
}


@InProceedings{CousotCousotLogozzo-Pre,
  author = 	 {Cousot, P{.} and Cousot, R{.} and Logozzo, F{.}},
  title = 	 {Contract Precondition Inference from Intermittent Assertions on Collections},
  booktitle = {VMCAI'11},
  year = 	 {2011},
  publisher = {Springer-Verlag}
}
 

@InProceedings{arrayal,
  author = 	 {Cousot, P{.} and Cousot, R{.} and Logozzo, F{.}},
  title = 	 {A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis},
  booktitle = {{ACM POPL'11} },
  year = 	 {2011},
  month = 	 jan,
  publisher = {{ACM} {P}ress}
}

@article{ppl,
  author    = {Bagnara, R{.} and
               Hill, P{.} M{.} and
               Zaffanella, E{.}},
  title     = {Applications of polyhedral computations to the analysis
               and verification of hardware and software systems},
  journal   = {Theor. Comput. Sci.},
  volume    = {410},
  number    = {46},
  year      = {2009}
}

@inproceedings{apron,
  author    = {Jeannet, B{.} and
               Min{\'e}, A{.}},
  title     = {Apron: A Library of Numerical Abstract Domains for Static
               Analysis},
  booktitle = {CAV'09}
 }

@inproceedings{ChenMineCousot08,
  author    = {Chen, L{.} and
               Min{\'e}, A{.} and
               Cousot, P{.}},
  title     = {A Sound Floating-Point Polyhedra Abstract Domain},
  booktitle = {APLAS'08},
  year      = {2008},
  publisher = {Springer-Verlag}
 }

@article{tracepartitioning,
  author    = {Rival, X{.} and
               Mauborgne, L{.}},
  title     = {The trace partitioning abstract domain},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {29},
  number    = {5},
  year      = {2007}
}

@inproceedings{verifast,
  author={Jacobs, Bart and Smans, Jan and Piessens, Frank},
  title={A Quick Tour of the {V}eri{F}ast Program Verifier},
  booktitle = {APLAS'10},
  year      = {2010},
}

@inproceedings{jstar,
 author = {Distefano, Dino and Parkinson J, Matthew J.},
 title = {j{S}tar: {T}owards practical verification for {J}ava},
 booktitle = {OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications},
 year = {2008},
 pages = {213--226},
 publisher = {ACM},
 }

@inproceedings{vericool,
 author = {Smans, Jan and Jacobs, Bart and Piessens, Frank},
 title = {{V}eri{C}ool: {A}n Automatic Verifier for a Concurrent Object-Oriented Language},
 booktitle = {FMOODS '08: Proceedings of the 10th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems},
 year = {2008},
 pages = {220--239},
 publisher = {Springer-Verlag},
 }


@inproceedings{MafLeino03,
  author    = {M{.} F{\"a}hndrich and
               K{.} R{.} M{.} Leino},
  title     = {Declaring and checking non-null types in an object-oriented
               language},
  booktitle = {{ACM OOPSLA}},
  year      = {2003},
}

@Misc{CLR,
  author = 	 {ECMA},
  title = 	 {{C}ommon {L}anguage {R}untime Specification},
  OPTmonth = 	 {},
  year = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

ANSI/ISO 9899-1990 American National Standard for Programming Languages - C, section 6.1.2.5
@Misc{C,
  OPTkey = 	 {},
  author = 	 {American National Standard for Programming Languages},
  title = 	 {The {C} language specification},
  OPThowpublished = {},
  OPTmonth = 	 {},
  year = 	 {1990},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{Martel02,
  author    = {M{.} Martel},
  title     = {Static Analysis of the Numerical Stability of Loops},
  booktitle = {SAS},
  year      = {2002},
  pages     = {133-150},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2477/24770133.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Martel02b,
  author    = {M{.} Martel},
  title     = {Propagation of Roundoff Errors in Finite Precision Computations:
               A Semantics Approach},
  booktitle = {ESOP},
  year      = {2002},
  pages     = {194-208},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2305/23050194.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Martel09,
  author    = {M{.} Martel},
  title     = {Program transformation for numerical precision},
  booktitle = {PEPM},
  year      = {2009},
  pages     = {101-110},
  ee        = {http://doi.acm.org/10.1145/1480945.1480960},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{GoubaultPutot11,
  author    = {E{.} Goubault and
               S{.} Putot},
  title     = {Static Analysis of Finite Precision Computations},
  booktitle = {VMCAI},
  year      = {2011},
  pages     = {232-247},
  ee        = {http://dx.doi.org/10.1007/978-3-642-18275-4_17},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{Monniaux08,
  author    = {D{.} Monniaux},
  title     = {The pitfalls of verifying floating-point computations},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {30},
  number    = {3},
  year      = {2008}
}




